\begin{tabbing}
$\forall$\=${\it es}$:event\_system\{i:l\}, $k$:Knd, $T$:Type, $l$:IdLnk, ${\it ds}$,${\it dt}$:fpf(Id; $x$.Type),\+
\\[0ex]$g$:((${\it tg}$:Id $\times$ (decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$(fpf{-}cap(${\it dt}$; id{-}deq; ${\it tg}$; void) List))) List).
\-\\[0ex]sends{-}p(${\it es}$; ${\it ds}$; $k$; $T$; $l$; ${\it dt}$; $g$) $\in$ prop\{i:l\}
\end{tabbing}